The present invention relates to a comparison and verification system by a computer, for comparing two logic circuits, preferably, upper and lower hierarchy logics in a hierarchy logic design, and a method thereof.
A logical design of a digital system is carried out with reference to a detailed logic drawing, and recently, a functional logic drawing in which contents ranked as an upper level than those in the above detailed logic are illustrated, has been frequently used. When the functional logic drawing is used for the logic design, a designer develops the functional logic drawing to the detailed logic drawing, and proceeds the design by a hierarchy manner. In the design procedure, a logical equivalence between the functional logic drawing ranked as an upper level and the detailed logic drawing ranked as a lower level must be verified.
There are the following methods of comparing and verifying an equivalence between an upper level logic and a lower level logic designed by a hierarchy logic, used by a computer, so far.
(i) A method in which a same test pattern is added to the upper logic and the lower logic to logically simulate same, and a coincidence check between the output patterns thereof is carried out.
(ii) A method in which Boolean expressions for output parameters are produced from the upper logic and the lower logic, converted into expressions by an addition standard form, and compared therebetween, or another method in which exclusive ORs of the Boolean expressions are obtained and compared same.
(iii) The upper logic and the lower logic are converted to logic forms, so called as a binary decision diagrams (BDDs), and an equivalence between the logic forms is verified.
The verification method on the basis of the BDD in above (iii) is dealt in, for example, S. B. Akers, "A PROCEDURE FOR FUNCTIONAL DESIGN VERIFICATION", Report of 10th International Symposium on Fault Tolerant Computing Conference. In this method BDDs are directly produced from a logical expression such as a logical circuit, a truth table or a Boolean expression, the processes of normalization, comparison, extraction and simplification are repeated to the produced BDDs by a plurality of times to carry out a comparison and verification.
The verification methods set forth above, however, suffers from the following disadvantages.
(i) In the method of comparing the results obtained by the logic simulation, a relatively long time is required for generating test patterns used for verifying a coincidence between the upper and lower layers.
(ii) In the method of comparing the Boolean expressions, a processing time and a required capacity of a memory respectively become order of N2, where N is the number of variables, as a result, if the number of the variables is increased, the method can not be substantially adopted.
(iii) In the method of using the BDD, a loop operation of the sequential processes such as the normalization, the comparison, the extraction and the simplification must be repeated until the coincidence is obtained, the processing time becomes K.N.log N, where K represents a repeat number, and N represents the number of nodes, and a very long processing time is required.